A:Type, eq:EqDecider(A), f,g:fpf(A; a.top), x:A, z:top.
sqequal(fpf-cap(fpf-join(eq; f; g); eq; x; z); fpf-cap(f; eq; x; fpf-cap(g; eq; x; z))) 

latex

Definitions	t  T, x:A. B(x), fpf-dom(eq; x; f), b, guard(T), P  Q, False, P  Q, A, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , Type, sqequal(s; t), x:A  B(x), EqDecider(T), fpf(A; a.B(a)), isect(A; x.B(x)), top, True, prop{i:l}, left + right, x.A(x), x. t(x), fpf-join(eq; f; g), x:AB(x), P  Q, P  Q, b, , s = t, Unit, void, fpf-cap(f; eq; x; z)
Lemmas	fpf wf, deq wf, fpf-join-ap-sq, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, not functionality wrt iff, fpf-join-dom, fpf-join wf, top wf, assert wf, fpf-dom wf